($\lambda$$T$,$L$,$P$,$z$. $\forall$$x$$\in$$L$. $P$($x$)) $\in$ $T$:Type$\rightarrow$($T$ List)$\rightarrow$($T$$\rightarrow$Prop)$\rightarrow\downarrow$True$\rightarrow$Prop